Due to the extreme strictness of dune (in particular the fact that (include_subdirs unqualified) never got implemented for Coq), I gave up on my attempts to improve the directory structure of the library, while remaining highly backwards compatible. So this is just documenting some structure and adding a CI job to ensure this documentation remains up to date. The chosen structure may not be perfect, but since we are not publishing any package, it can be easily refined later (c.f. dev/doc/structure.md).

WTF are all these added new files? Why is there a committed generated file (the .dot)?

WTF are all these added new files?

Just symlinks needed by the CI job (and ignored by dune) to check the subcomponents structure. Since dune forbids to change the directory structure without chaning the logical names (i.e. having some impact in terms of backward compatibility), those are needed for the CI job (based on coq_makefile) to compile parts of some directories in different subcomponents. (it's all documented in dev/doc/structure.md)

Why is there a committed generated file (the .dot)?

It's not entirely generated, in particular the compat subcomponent doesn't actually depend on everything (according to coqdep), but we want to declare it as possibly depending from everything, because any future compat file could add a dependency on virtually anything.